feat(Topology/Connected): local (path-)connectedness of products and pi types by korbonits · Pull Request #41663 · leanprover-community/mathlib4

korbonits · 2026-07-12T22:03:01Z

Add product and pi instances for LocallyConnectedSpace and LocallyPathConnectedSpace, together with a full characterization of local (path-)connectedness of pi types:

Prod.locallyConnectedSpace / Prod.locallyPathConnectedSpace: binary products.
Pi.locallyConnectedSpace_of_finite_nonpreconnected / Pi.locallyPathConnectedSpace_of_finite_nonpathconnected: a product of locally (path-)connected spaces is locally (path-)connected provided all but finitely many factors are preconnected (resp. path-connected). The Finite ι and all-factors-preconnected (resp. path-connected) instances are corollaries.
Pi.locallyConnectedSpace_iff / Pi.locallyPathConnectedSpace_iff: a product is locally (path-)connected iff it is empty or the above conditions hold.
Topology.IsQuotientMap.locallyConnectedSpace: quotients of locally connected spaces are locally connected (used for the forward direction via the projections; the analogous IsQuotientMap.locallyPathConnectedSpace already existed).

Follow-up to #40092.

AI disclosure

level: Level 5 / Level 6 in the link shared -- I feel confident about the math but I am still learning Lean itself
code: most of the Lean in this PR was drafted by Claude Code (statements, proofs, docstrings).
direction and review: I chose the contribution, made the decisions (e.g., PathConnectedSpace for the path-side hypothesis, strengthening the helper to quotient maps, deferring Quot instances), reviewed every line, and wrote all GitHub/Zulip comments.
testing: I ran local lake build of files and lake env lean of some test files (uncommitted)

… are locally (path-)connected

github-actions · 2026-07-12T22:03:09Z

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

github-actions · 2026-07-12T22:04:26Z

PR summary 2ab6a13e5d

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff (regex)

+ Pi.locallyConnectedSpace
+ Pi.locallyConnectedSpace_iff
+ Pi.locallyConnectedSpace_of_finite
+ Pi.locallyConnectedSpace_of_finite_nonpreconnected
+ Pi.locallyPathConnectedSpace
+ Pi.locallyPathConnectedSpace_iff
+ Pi.locallyPathConnectedSpace_of_finite
+ Pi.locallyPathConnectedSpace_of_finite_nonpathconnected
+ Prod.locallyConnectedSpace
+ Prod.locallyPathConnectedSpace
+ Topology.IsQuotientMap.locallyConnectedSpace

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 2ab6a13).

+11 new declarations
−0 removed declarations

+Pi.locallyConnectedSpace
+Pi.locallyConnectedSpace_iff
+Pi.locallyConnectedSpace_of_finite
+Pi.locallyConnectedSpace_of_finite_nonpreconnected
+Pi.locallyPathConnectedSpace
+Pi.locallyPathConnectedSpace_iff
+Pi.locallyPathConnectedSpace_of_finite
+Pi.locallyPathConnectedSpace_of_finite_nonpathconnected
+Prod.locallyConnectedSpace
+Prod.locallyPathConnectedSpace
+Topology.IsQuotientMap.locallyConnectedSpace

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 2ab6a13e5d
Reference commit fd1d54bcac

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

… -- edit for concision

korbonits · 2026-07-12T22:36:36Z

LLM-generated

CoolRmal

I think here's a better design. May you first prove the following?

theorem Pi.locallyConnectedSpace_of_finite_nonpreconnected
    [∀ i, TopologicalSpace (X i)] [∀ i, LocallyConnectedSpace (X i)]
    (hfinite : {i | ¬PreconnectedSpace (X i)}.Finite) : LocallyConnectedSpace (∀ i, X i) := sorry

which is saying that if every X i is locally connected and the set of i such that X i is not preconnected is finite, then LocallyConnectedSpace (∀ i, X i). Pi.locallyConnectedSpace_of_finite and Pi.locallyConnectedSpace should then be easy corollaries.

You can then do something similar for locally path connected space.

CoolRmal · 2026-07-14T22:28:32Z

awaiting-author

CoolRmal · 2026-07-15T03:41:38Z

And maybe if you want you can also prove the following characterization of locally connectedness of the product: ∀ i, X i is locally connected if either it is empty or every X i is locally connected and {i | ¬PreconnectedSpace (X i)}.Finite. To prove this I think you need to show first that if f : X → Y is open continuous surjective and X is locally connected, then so is Y.

korbonits · 2026-07-15T06:51:54Z

And maybe if you want you can also prove the following characterization of locally connectedness of the product: ∀ i, X i is locally connected if either it is empty or every X i is locally connected and {i | ¬PreconnectedSpace (X i)}.Finite. To prove this I think you need to show first that if f : X → Y is open continuous surjective and X is locally connected, then so is Y.

Is it OK if I do this in a follow-up PR or would you prefer to see it in this PR? I can commit to that as a fast follow. I think the helper lemma deserves its own visibility! Open to your thoughts here :) @CoolRmal

CoolRmal · 2026-07-15T17:04:26Z

I think it is fine to include these lemmas in this single PR, but maybe you can change the PR description a little bit.

grunweg · 2026-07-16T11:38:01Z

Hello from triage! Can you comment on whether you used AI for this project (and if so, label with PR with LLM-generated)? Thanks! (Per mathlib's AI policy, this is not forbidden in principle, but its usage must be disclosed.)

korbonits · 2026-07-16T14:16:59Z

@grunweg -- correct! I added the LLM-generated tag after pushing the PR to make sure it was tagged correctly. Let me know if there's anything I can do to provide more transparency about my AI usage.

grunweg · 2026-07-16T15:32:03Z

@grunweg -- correct! I added the LLM-generated tag after pushing the PR to make sure it was tagged correctly. Let me know if there's anything I can do to provide more transparency about my AI usage.

Thanks. Can you also describe how you used AI in the PR description, below the fold? (This scale has some categories that may be helpful.)

…cted-prod

CoolRmal · 2026-07-16T17:59:34Z

You should remove the awaiting author label if you want another round of review.

korbonits · 2026-07-16T18:24:42Z

-awaiting-author

CoolRmal

I only give comments for LocallyConnectedSpace, but these should also apply to LocallyPathConnectedSpace.

CoolRmal · 2026-07-19T22:36:56Z

+/-- The image of a locally connected space under a quotient map (in particular, under an open
+continuous surjection) is locally connected. -/


Suggested change

/-- The image of a locally connected space under a quotient map (in particular, under an open

continuous surjection) is locally connected. -/

/-- The image of a locally connected space under a quotient map is locally connected. -/

I think there's no need to mention that an open continuous surjection is a quotient map.

CoolRmal · 2026-07-19T23:04:41Z

+  rw [locallyConnectedSpace_iff_connectedComponentIn_open]
+  intro F hF y _
+  rw [← hf.isOpen_preimage, isOpen_iff_mem_nhds]
+  intro x hx
+  have hxF : x ∈ f ⁻¹' F := connectedComponentIn_subset F y hx
+  refine Filter.mem_of_superset
+    ((hF.preimage hf.continuous).connectedComponentIn.mem_nhds (mem_connectedComponentIn hxF))
+    fun z hz ↦ ?_
+  rw [mem_preimage, connectedComponentIn_eq hx]
+  exact connectedComponentIn_mono _ (image_preimage_subset f F)
+    (hf.continuous.mapsTo_connectedComponentIn hxF hz)


This long proof suggests that we are missing some APIs. Here's a potentially better way to do this:

Prove this formula for the preimage of a connected component : f ⁻¹' connectedComponentIn F y = ⋃ x ∈ f ⁻¹' connectedComponentIn F y, connectedComponentIn (f ⁻¹' F) x.

We want to show that IsOpen (connectedComponentIn F y), and as f is a quotient map it suffices to show that f ⁻¹' connectedComponentIn F y is open, and by the formula above we know that it is open because it is the union of open sets (where openness of connectedComponentIn (f ⁻¹' F) x follows from the [LocallyConnectedSpace α]).

Moreover, from this proof you can see that we can replace IsQuotientMap f with IsCoinducing f (surjection is not needed; see Topology.isQuotientMap_iff).

CoolRmal · 2026-07-19T23:05:29Z

+    · haveI := hloc
+      exact Pi.locallyConnectedSpace_of_finite_nonpreconnected hfin


Suggested change

· haveI := hloc

exact Pi.locallyConnectedSpace_of_finite_nonpreconnected hfin

· exact locallyConnectedSpace_of_finite_nonpreconnected hfin

CoolRmal · 2026-07-19T23:35:57Z

+  rw [nhds_pi, Filter.mem_pi] at hU
+  obtain ⟨J, hJ, t, ht, htU⟩ := hU
+  classical
+  set K := J ∪ {i | ¬PreconnectedSpace (X i)} with hK


Suggested change

set K := J ∪ {i | ¬PreconnectedSpace (X i)} with hK

let K := J ∪ {i | ¬PreconnectedSpace (X i)}

And then hK is not needed. As K is not really used a lot of times I think it also makes sense to replace K with J ∪ {i | ¬PreconnectedSpace (X i)} in the proof, but this is optional.

CoolRmal · 2026-07-19T23:42:51Z

+  rw [locallyConnectedSpace_iff_connected_subsets]
+  intro x U hU


Suggested change

rw [locallyConnectedSpace_iff_connected_subsets]

intro x U hU

refine locallyConnectedSpace_iff_connected_subsets.2 fun x U hU ↦ ?_

More concise

CoolRmal · 2026-07-19T23:44:00Z

+  refine ⟨K.pi fun i ↦ connectedComponentIn (t i) (x i),
+    set_pi_mem_nhds (hJ.union hfinite) fun i _ ↦ connectedComponentIn_mem_nhds (ht i), ?_,
+    fun f hf ↦ htU fun i hiJ ↦ connectedComponentIn_subset _ _ (hf i (mem_union_left _ hiJ))⟩
+  rw [← univ_pi_piecewise_univ]


May you move classical just before this line (as this is the lemma that uses classical)?

CoolRmal · 2026-07-19T23:50:50Z

+    suffices himg : Function.eval i '' connectedComponent x = univ by
+      exact ⟨himg ▸ isPreconnected_connectedComponent.image _ (continuous_apply i).continuousOn⟩


Suggested change

suffices himg : Function.eval i '' connectedComponent x = univ by

exact ⟨himg ▸ isPreconnected_connectedComponent.image _ (continuous_apply i).continuousOn⟩

suffices himg : Function.eval i '' connectedComponent x = univ from

⟨himg ▸ isPreconnected_connectedComponent.image _ (continuous_apply i).continuousOn⟩

by exact is not preferred.

CoolRmal · 2026-07-19T23:51:09Z

+    refine (subset_univ _).antisymm fun z _ ↦
+      ⟨Function.update x i z, htV fun j hj ↦ ?_, by simp⟩


Suggested change

refine (subset_univ _).antisymm fun z _ ↦

⟨Function.update x i z, htV fun j hj ↦ ?_, by simp⟩

refine (subset_univ _).antisymm fun z _ ↦ ⟨Function.update x i z, htV fun j hj ↦ ?_, by simp⟩

No need for a line break like this.

CoolRmal · 2026-07-19T23:53:23Z

awaiting-author

feat(Topology/Connected): products of locally (path-)connected spaces…

4f96597

… are locally (path-)connected

github-actions Bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Jul 12, 2026

github-actions Bot added the t-topology Topological spaces, uniform spaces, metric spaces, filters label Jul 12, 2026

feat(Topology/Connected): products of locally (path-)connected spaces…

4075c78

… -- edit for concision

github-actions Bot added the LLM-generated PRs with substantial input from LLMs - review accordingly label Jul 12, 2026

CoolRmal self-assigned this Jul 14, 2026

CoolRmal reviewed Jul 14, 2026

View reviewed changes

Comment thread Mathlib/Topology/Connected/LocallyConnected.lean Outdated

github-actions Bot added the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 14, 2026

responding to @CoolRmal's generous feedback

8db06a8

korbonits changed the title ~~feat(Topology/Connected): products of locally (path-)connected spaces are locally (path-)connected~~ feat(Topology/Connected): local (path-)connectedness of products and pi types Jul 15, 2026

Merge branch 'master' into loc-connected-prod

f16796e

korbonits requested a review from CoolRmal July 15, 2026 06:53

korbonits added 2 commits July 16, 2026 10:51

following up with additional commit per @CoolRmal feedback

dd50e61

Merge remote-tracking branch 'fork/loc-connected-prod' into loc-conne…

1ea6919

…cted-prod

github-actions Bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 16, 2026

korbonits and others added 3 commits July 16, 2026 11:55

fixing logical error in docstrings

3e13aff

Merge branch 'master' into loc-connected-prod

cad501e

Merge branch 'master' into loc-connected-prod

2ab6a13

CoolRmal reviewed Jul 19, 2026

View reviewed changes

github-actions Bot added the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 19, 2026

		/-- The image of a locally connected space under a quotient map (in particular, under an open
		continuous surjection) is locally connected. -/

		· haveI := hloc
		exact Pi.locallyConnectedSpace_of_finite_nonpreconnected hfin

	· haveI := hloc
	exact Pi.locallyConnectedSpace_of_finite_nonpreconnected hfin
	· exact locallyConnectedSpace_of_finite_nonpreconnected hfin

	set K := J ∪ {i \| ¬PreconnectedSpace (X i)} with hK
	let K := J ∪ {i \| ¬PreconnectedSpace (X i)}

		rw [locallyConnectedSpace_iff_connected_subsets]
		intro x U hU

	rw [locallyConnectedSpace_iff_connected_subsets]
	intro x U hU
	refine locallyConnectedSpace_iff_connected_subsets.2 fun x U hU ↦ ?_

		suffices himg : Function.eval i '' connectedComponent x = univ by
		exact ⟨himg ▸ isPreconnected_connectedComponent.image _ (continuous_apply i).continuousOn⟩

		refine (subset_univ _).antisymm fun z _ ↦
		⟨Function.update x i z, htV fun j hj ↦ ?_, by simp⟩

Uh oh!

Conversation

korbonits commented Jul 12, 2026 • edited by grunweg Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Jul 12, 2026

Welcome new contributor!

Uh oh!

github-actions Bot commented Jul 12, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 2ab6a13e5d

Import changes for modified files

Declarations diff (regex)

Declarations diff (Lean)

Uh oh!

korbonits commented Jul 12, 2026

Uh oh!

CoolRmal left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

CoolRmal commented Jul 14, 2026

Uh oh!

CoolRmal commented Jul 15, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

korbonits commented Jul 15, 2026

Uh oh!

CoolRmal commented Jul 15, 2026

Uh oh!

grunweg commented Jul 16, 2026

Uh oh!

korbonits commented Jul 16, 2026

Uh oh!

grunweg commented Jul 16, 2026

Uh oh!

CoolRmal commented Jul 16, 2026

Uh oh!

korbonits commented Jul 16, 2026

Uh oh!

CoolRmal left a comment

Choose a reason for hiding this comment

Uh oh!

CoolRmal Jul 19, 2026

Choose a reason for hiding this comment

Uh oh!

CoolRmal Jul 19, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

CoolRmal Jul 19, 2026

Choose a reason for hiding this comment

Uh oh!

CoolRmal Jul 19, 2026

Choose a reason for hiding this comment

Uh oh!

CoolRmal Jul 19, 2026

Choose a reason for hiding this comment

Uh oh!

CoolRmal Jul 19, 2026

Choose a reason for hiding this comment

Uh oh!

CoolRmal Jul 19, 2026

Choose a reason for hiding this comment

Uh oh!

CoolRmal Jul 19, 2026

Choose a reason for hiding this comment

Uh oh!

CoolRmal commented Jul 19, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

korbonits commented Jul 12, 2026 •

edited by grunweg

Loading

github-actions Bot commented Jul 12, 2026 •

edited

Loading

CoolRmal left a comment •

edited

Loading

CoolRmal commented Jul 15, 2026 •

edited

Loading

CoolRmal Jul 19, 2026 •

edited

Loading